Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:		f(f(y,z),f(x,f(a,x)))	→ f(f(f(a,z),f(x,a)),f(a,y))

There are 5 dependency pairs:


2:		F(f(y,z),f(x,f(a,x)))	→ F(f(f(a,z),f(x,a)),f(a,y))
3:		F(f(y,z),f(x,f(a,x)))	→ F(f(a,z),f(x,a))
4:		F(f(y,z),f(x,f(a,x)))	→ F(a,z)
5:		F(f(y,z),f(x,f(a,x)))	→ F(x,a)
6:		F(f(y,z),f(x,f(a,x)))	→ F(a,y)

The approximated dependency graph contains one SCC: {2,3}.

Consider the SCC {2,3}. The constraints could not be solved.

Tyrolean Termination Tool (0.01 seconds) --- May 3, 2006